es:ES, R:{R:EE| e, e':E. R(e,e')  (e' < e)} , d:(e, e':E. Dec(R(e,e'))).
es-r-pred{i:l}(es;d;R)  E(E + Top) 

latex

Definitions	left + right, Top, Dec(P), {x:A| B(x)} , E, P  Q, x:AB(x), x(s1,s2), f(a), , Type, (e < e'), x:A. B(x), t  T, ES, es-r-pred{i:l}(es;d;R), causal-pred-from-relation, P & Q, P  Q, x:A. B(x), x:A  B(x), causal-predecessor(es;p), s = t, b
Lemmas	event system wf, es-causl wf, es-E wf, decidable wf